from tc_python.arule import ARule
from tc_python.frule import FRule
from t_core.messages import Packet
from t_core.matcher import Matcher

from itertools import *

from himesis_utils import *
from core.himesis import Himesis

from copy import deepcopy

from collapse_backward import *

# build the transformation using the individual rules
# each layer is represented by a list of rules and the transformation is a list of layers

class SymbolicStateSpace():
    """
    Builds the state space for a transformation
    
    Attributes:
        - backwardMatchCache: holds a dictionary cache that allows checking whether a backward link pattern matches a rule
                              key: concatenation of the backward link pattern name and the rule name
                              value: True, False, meaning the backward links patterns matches or does not match.
        - symbStateSpace: holds the state space itself. The state space is a list of lists of rules, obtained by going through
                          each layer, calculating its powerset and for each state in that powerset merging it will all states
                          found in previous layers. A merge can only be achieved if all the backward linked graphs in the
                          new state exist the previous state.
                          
    """
    
    def __init__(self, transformation, rulesIncludingBackwardLinks, backwardPatterns):
        # load the transformation
        self.transformation = transformation
        self.rulesIncludingBackwardLinks = rulesIncludingBackwardLinks
        self.backwardPatterns = backwardPatterns 
        self.symbStateSpace = []        
        self.backwardMatchCache = {}


    def build_set(self):     
                         
        for curLayer in range(len(self.transformation)):
            # first build the traceability links for all the rules in the layer
            # self._printRules(self.transformation[layer])           
            # layerWithTraceLinks = self._buildTraceabilityLinks(layer)
            
            # if we're dealing with the first layer then just add the powerset of the rules
            # in the first layer as the first set of symbolic states in the state space
            
            if curLayer == 0:
                # build the powerset of all the rules in the first layer
                self.symbStateSpace.extend(self._rulePowerSet(self.transformation[curLayer]))

            else:
                # build the powerset of all the rules in the layer in a temporary variable
                # remove the empty rule application since it does nothing
                curLayerSymbStateSpace = self._rulePowerSet(self.transformation[curLayer]) 
                curLayerSymbStateSpace = [x for x in curLayerSymbStateSpace if x <> ()]
                
                # the new states will only be added at the end of the layer being processed
                statesToAdd = []        
 
                # go through the symbolic states of the current layer
                for curSymbState in range(len(curLayerSymbStateSpace)):                
                    
                    # check if the symbolic state we're analysing in the current layer has any of the backward link rules
                    matchBack = []
                    for ruleInclBack in self.rulesIncludingBackwardLinks[curLayer]:
                        # gather all the back rules belonging to the curSymbState so the search up can begin
                        if ruleInclBack in set(curLayerSymbStateSpace[curSymbState]):
                            matchBack.extend(self.backwardPatterns[ruleInclBack.__class__.__name__])
                    
                    # go through the symbolic states of the previous layer       
                    for previousSymbState in range(len(self.symbStateSpace)):

                        # try to eliminate backward link rules on the previous symbolic state                      
                        foundMatchBack = list(matchBack)
                        
                        cacheKeys = self._buildCacheKeys(matchBack,self.symbStateSpace[previousSymbState])
                      
                        # the matchers are organised by backward link pattern
                        for matcher in range(len(cacheKeys)):
                            
                            for key in cacheKeys[matcher]:

                                # check cache first
                                if key[0] in set(self.backwardMatchCache.keys()):
#                                    print 'Cache Hit!'
                                    if self.backwardMatchCache[key[0]] == True:
                                        # set the backward match pattern in search list to None because it has been found
                                        foundMatchBack[matcher] = None
                                        break
                                else:
#                                   print 'Cache Miss!'                                    
                                    # perform the match using T-Core and add the result (true/false) to the cache
                                    p = Packet()
                                    p.graph = self.symbStateSpace[previousSymbState][key[1]]
                                    p = matchBack[matcher].packet_in(p)
                                    self.backwardMatchCache.update({key[0]:matchBack[matcher].is_success})
                                    if matchBack[matcher].is_success == True:
                                        foundMatchBack[matcher] = None
                                        break

                                    
                            # compress the matchBack list by removing all the None elements
                            # (corresponding backward patterns required by the curSymbolicState found on this layer)
                            compressed = [x for x in foundMatchBack if x <> None]
                            if compressed == []:
                                foundMatchBack = []
                                break
                        
                        # if all the backward link matches were found going up the state space then  
                        # we can add the rules in the current symbolic state to the symbolic state in the previous layer    
                                                 
                        if foundMatchBack == []:                           
                            realPreviousSymbState = self.symbStateSpace[previousSymbState]
                            realPreviousSymbState += curLayerSymbStateSpace[curSymbState] 
                            statesToAdd.append(realPreviousSymbState)                                               
                
                # finally add the new states to the global state space
                self.symbStateSpace.extend(statesToAdd)


    def verify_property(self, propIsolatedElems, propMatchPattern, propTotal):
        """
        check a property in the state space
        1) build the united graph from the symbolic state
        2) build all collapsed graph from the initial graph
        3) check that if the precondition of the property holds in any of the collapsed graphs,
           then the postcondition also hold. If it is not the case for one graph then return false. Else return true.
        For efficiency, and because collapsing is expensive, do a preprocessing step that only collapses a state if all
        elements included in the property are also included in the state
        
        Parameters:
            propIsolatedElems: query that matches in a state just the match elements in the property
            propMatchPattern: query that matches in a state the match pattern in the property
            propTotal: query that matches in a state the whole property
        """

        isolated = Matcher(propIsolatedElems)
        match = Matcher(propMatchPattern)
        total = Matcher(propTotal)

        state_index = 0
        
        found_counterexample = False
        
        for state in self.symbStateSpace:
            if state != ():
                merged_state = deepcopy(state[0])
                rule_index = 1
                
                # go through all the rules in the layer and merge them in one graph
                while rule_index < len(state):
                    merged_state = merge_models(merged_state, state[rule_index])
                    rule_index += 1
            
                s = Packet()
                s.graph = deepcopy(merged_state)
                
#                graph_to_dot('out' + str(state_index), s.graph)                
                
                isolated.packet_in(s)

                if isolated.is_success:
                    print 'State ' + str(state_index)
                    print '    Found Property Elements'

                    # build set of collapsed states to analyse
                    states_to_analyse = [merged_state] 
                    states_to_analyse.extend(collapse_backward(s))
                    
                    print '    Number of states to analyse: ' + str(len(states_to_analyse))
                    for collapsed_state in range(len(states_to_analyse)):
                        s = Packet()
                        s.graph = states_to_analyse[collapsed_state]
                        
                        graph_to_dot('out' + str(state_index) + '.' + str(collapsed_state), s.graph)
                        
                        match.packet_in(s)
                        
                        print '    Collapsed state ' + str(collapsed_state)                      
                        # if the match was found, try to find the whole property
                        if match.is_success:
                            print '        Found Match!'
                            total.packet_in(s)
                            if total.is_success:
                                print '        Found Apply!'
                            else:
                                print '        Could not find Apply!'
                                found_counterexample = True
                                # match part of the property was found, but apply not, thus we found a counterexample
                                break
                        else:
                            print '        Could not find Match!'
                            
                else:
                    print 'State ' + str(state_index)
                    print '    Property Elements not found'            
            
                if found_counterexample == True:
                    break
                state_index += 1

        print '\n'
        if found_counterexample == True:
            print 'Property does not Hold!!!'
        else:
            print 'Property Holds!!!'
            


    def _rulePowerSet(self,rules):
        return list(chain.from_iterable(combinations(rules, r) for r in range(len(rules)+1)))
        
    def _buildTraceabilityLinks(self,layer):
        """
        build traceability (for the time being apply all rules until exhaustion)
        """
        symbLayer = []
        for rule in layer:
            p = Packet()
            p.graph = rule
            for transf in self.traceBuildTransf:
                p = transf.packet_in(p)
            symbLayer.append(p)
        return symbLayer
    

    def _buildCacheKeys(self, matchBack, symbState):
        """
        build a set of cache keys by concatenating the name of the backward link matcher with the rule to check
        build one list per key, to avoid rematching keys that were already found
        """     
        cacheKeys = []
        for match in range(len(matchBack)):
            cacheKeys.append([])
            for state in range(len(symbState)):
                cacheKeys[match].append((matchBack[match].condition.__class__.__name__ + symbState[state].__class__.__name__, state))
        return cacheKeys


    def _eliminate_repeated_collapse_matches(self, match_set):
        """
        remove permutation of the same two elements to collapse from a match set
        """
        new_match_set = []
        for i in range(0, len(match_set)):
            found_repeated = False
            for j in range(0, i):
                if match_set[i]['1'] == match_set[j]['2'] and match_set[i]['2'] == match_set[j]['1']:
                    found_repeated = True
                    break
            if not found_repeated:
                new_match_set.append(match_set[i])
        return new_match_set



#verify_property()          

# auxiliary structures    

# the transformation with layers having rules inside
#transformation = [[HL1_S2S(), HL1_S2S(), HL1_S2S(), HL1_M2M(), HL1_M2M(), HL2_F2F()], [HL2_SM2SM(), HL2_SM2SM(), HL2_MM2MM(), HL2_MM2MM(), HL2_F2F(), HL2_F2F(), HL2_F2F()]]
#transformation = [[HL1_S2S(), HL1_M2M()], [HL2_SM2SM()]]
#transformation = [[HL1_S2S()], [HL2_SM2SM()]]

# rules including backward links, per layer
#rulesIncludingBackLinks = [[],[transformation[1][0], transformation[1][1], transformation[1][2], transformation[1][3]]]
#rulesIncludingBackLinks = [[],[transformation[1][0]]]

# match rules allowing to verify if the backward links exist at any point previously
# during the symbolic execution. Associated to the name of a transformation rule
#backwardPatterns = {'HL1_S2S': None,
#                    'HL1_M2M': None,                   
#                    'HL2_SM2SM': [Matcher(HMatch_L2_SM2SM_S2SLHS()),Matcher(HMatch_L2_SM2SM_M2MLHS())],
#                    'HL2_MM2MM': [Matcher(HMatch_L2_MM2MM_M2M_1LHS()),Matcher(HMatch_L2_MM2MM_M2M_2LHS())],
#                    'HL2_F2F': None}
#
#s = SymbolicStateSpace(transformation, rulesIncludingBackLinks, backwardPatterns)
#t0 = time.time()
#res = s.build_set()
#print len(s.symbStateSpace)
#t1 = time.time()
#print 'Done in: ' + str(t1 -t0)
#
#for state in s.symbStateSpace:
#    print "----------"
#    for s in state:
#        print s



#x =  HL2_F2F()
# 
#print x in set([HL2_SM2SM(), HL2_MM2MM(), x])


#backwardPatterns = [[None,None],[[HMatch_S2SLHS(),HMatch_M2MLHS()],[HMatch_M2MLHS()]]]

#s = SymbolicStateSpace(transformation, None)
#s.build()

#print(list(s.stateSpace))

#f=FRule(HBuild_back_F2FLHS(),HBuild_back_F2FRHS())
#p = Packet()
#p.graph = HL2_F2F()
#print p
#p1 = f.packet_in(p)
#print p1
#
#print f.is_success
#
#if f.exception:
#    raise f.exception
#
#a = Matcher(HMatch_M2MLHS())
#
#p = Packet()
#p.graph = HL1_S2S()
#p1 = a.packet_in(p)
#print p1
#
#print a.is_success
#
#if a.exception:
#    raise a.exception
#
#b = ARule(HBuild_back_S2SLHS(),HBuild_back_S2SRHS())
#
#p2 = Packet()
#p2.graph = HL1_S2S()
#p3 = b.packet_in(p2)
#print p3
#
#print b.is_success
#
#if b.exception:
#    raise b.exception
